Search Results

Documents authored by Majumdar, Rupak

Found 2 Possible Name Variants:

Majumdar, Rupak M.

Document
DOI: 10.4230/DagRep.2.11.45
Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461)

Authors: Nikolaj Bjorner, Krishnendu Chatterjee, Laura Kovacs, and Rupak M. Majumdar

Published in: Dagstuhl Reports, Volume 2, Issue 11 (2013)

Abstract
This report documents the program and the outcomes of the Dagstuhl Seminar 12461 "Games and Decisions for Rigorous Systems Engineering". The seminar brought together researchers working in rigorous software engineering, with a special focus on the interaction between synthesis and automated deduction. This event was the first seminar of this kind and a kickoff of a series of seminars organised on rigorous systems engineering. The theme of the seminar was close in spirit to many events that have been held over the last decades. The talks scheduled during the seminar naturally reflected fundamental research themes of the involved communities.
Cite as

Nikolaj Bjorner, Krishnendu Chatterjee, Laura Kovacs, and Rupak M. Majumdar. Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461). In Dagstuhl Reports, Volume 2, Issue 11, pp. 45-65, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Article{bjorner_et_al:DagRep.2.11.45,
  author =	{Bjorner, Nikolaj and Chatterjee, Krishnendu and Kovacs, Laura and Majumdar, Rupak M.},
  title =	{{Games and Decisions for Rigorous Systems Engineering (Dagstuhl Seminar 12461)}},
  pages =	{45--65},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{2},
  number =	{11},
  editor =	{Bjorner, Nikolaj and Chatterjee, Krishnendu and Kovacs, Laura and Majumdar, Rupak M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.2.11.45},
  URN =		{urn:nbn:de:0030-drops-39092},
  doi =		{10.4230/DagRep.2.11.45},
  annote =	{Keywords: Systems Engineering, Software Verification, Reactive Synthesis, Automated Deduction}
}

Majumdar, Rupak

Document
DOI: 10.4230/LIPIcs.FSTTCS.2023.42
Counter Machines with Infrequent Reversals

Authors: Alain Finkel, Shankara Narayanan Krishna, Khushraj Madnani, Rupak Majumdar, and Georg Zetzsche

Published in: LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)

Abstract
Bounding the number of reversals in a counter machine is one of the most prominent restrictions to achieve decidability of the reachability problem. Given this success, we explore whether this notion can be relaxed while retaining decidability. To this end, we introduce the notion of an f-reversal-bounded counter machine for a monotone function f: ℕ → ℕ. In such a machine, every run of length n makes at most f(n) reversals. Our first main result is a dichotomy theorem: We show that for every monotone function f, one of the following holds: Either (i) f grows so slowly that every f-reversal bounded counter machine is already k-reversal bounded for some constant k or (ii) f belongs to Ω(log(n)) and reachability in f-reversal bounded counter machines is undecidable. This shows that classical reversal bounding already captures the decidable cases of f-reversal bounding for any monotone function f. The key technical ingredient is an analysis of the growth of small solutions of iterated compositions of Presburger-definable constraints. In our second contribution, we investigate whether imposing f-reversal boundedness improves the complexity of the reachability problem in vector addition systems with states (VASS). Here, we obtain an analogous dichotomy: We show that either (i) f grows so slowly that every f-reversal-bounded VASS is already k-reversal-bounded for some constant k or (ii) f belongs to Ω(n) and the reachability problem for f-reversal-bounded VASS remains Ackermann-complete. This result is proven using run amalgamation in VASS. Overall, our results imply that classical restriction of reversal boundedness is a robust one.
Cite as

Alain Finkel, Shankara Narayanan Krishna, Khushraj Madnani, Rupak Majumdar, and Georg Zetzsche. Counter Machines with Infrequent Reversals. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 42:1-42:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{finkel_et_al:LIPIcs.FSTTCS.2023.42,
  author =	{Finkel, Alain and Krishna, Shankara Narayanan and Madnani, Khushraj and Majumdar, Rupak and Zetzsche, Georg},
  title =	{{Counter Machines with Infrequent Reversals}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{42:1--42:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-304-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{284},
  editor =	{Bouyer, Patricia and Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.42},
  URN =		{urn:nbn:de:0030-drops-194152},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.42},
  annote =	{Keywords: Counter machines, reversal-bounded, reachability, decidability, complexity}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.23
Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete

Authors: Shankara Narayanan Krishna, Khushraj Nanik Madnani, Rupak Majumdar, and Paritosh Pandya

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
We investigate the decidability of the {0,∞} fragment of Timed Propositional Temporal Logic (TPTL). We show that the satisfiability checking of TPTL^{0,∞} is PSPACE-complete. Moreover, even its 1-variable fragment (1-TPTL^{0,∞}) is strictly more expressive than Metric Interval Temporal Logic (MITL) for which satisfiability checking is EXPSPACE complete. Hence, we have a strictly more expressive logic with computationally easier satisfiability checking. To the best of our knowledge, TPTL^{0,∞} is the first multi-variable fragment of TPTL for which satisfiability checking is decidable without imposing any bounds/restrictions on the timed words (e.g. bounded variability, bounded time, etc.). The membership in PSPACE is obtained by a reduction to the emptiness checking problem for a new "non-punctual’’ subclass of Alternating Timed Automata with multiple clocks called Unilateral Very Weak Alternating Timed Automata (VWATA^{0,∞}) which we prove to be in PSPACE. We show this by constructing a simulation equivalent non-deterministic timed automata whose number of clocks is polynomial in the size of the given VWATA^{0,∞}.
Cite as

Shankara Narayanan Krishna, Khushraj Nanik Madnani, Rupak Majumdar, and Paritosh Pandya. Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{krishna_et_al:LIPIcs.CONCUR.2023.23,
  author =	{Krishna, Shankara Narayanan and Madnani, Khushraj Nanik and Majumdar, Rupak and Pandya, Paritosh},
  title =	{{Satisfiability Checking of Multi-Variable TPTL with Unilateral Intervals Is PSPACE-Complete}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.23},
  URN =		{urn:nbn:de:0030-drops-190171},
  doi =		{10.4230/LIPIcs.CONCUR.2023.23},
  annote =	{Keywords: TPTL, Satisfiability, Non-Punctuality, Decidability, Expressiveness, ATA}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ICALP.2023.3
Context-Bounded Analysis of Concurrent Programs (Invited Talk)

Authors: Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
Context-bounded analysis of concurrent programs is a technique to compute a sequence of under-approximations of all behaviors of the program. For a fixed bound k, a context bounded analysis considers only those runs in which a single process is interrupted at most k times. As k grows, we capture more and more behaviors of the program. Practically, context-bounding has been very effective as a bug-finding tool: many bugs can be found even with small bounds. Theoretically, context-bounded analysis is decidable for a large number of programming models for which verification problems are undecidable. In this paper, we survey some recent work in context-bounded analysis of multithreaded programs. In particular, we show a general decidability result. We study context-bounded reachability in a language-theoretic setup. We fix a class of languages (satisfying some mild conditions) from which each thread is chosen. We show context-bounded safety and termination verification problems are decidable iff emptiness is decidable for the underlying class of languages and context-bounded boundedness is decidable iff finiteness is decidable for the underlying class.
Cite as

Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. Context-Bounded Analysis of Concurrent Programs (Invited Talk). In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 3:1-3:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{baumann_et_al:LIPIcs.ICALP.2023.3,
  author =	{Baumann, Pascal and Ganardi, Moses and Majumdar, Rupak and Thinniyam, Ramanathan S. and Zetzsche, Georg},
  title =	{{Context-Bounded Analysis of Concurrent Programs}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{3:1--3:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.3},
  URN =		{urn:nbn:de:0030-drops-180559},
  doi =		{10.4230/LIPIcs.ICALP.2023.3},
  annote =	{Keywords: Context-bounded analysis, Multi-threaded programs, Decidability}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.110
Checking Refinement of Asynchronous Programs Against Context-Free Specifications

Authors: Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
In the language-theoretic approach to refinement verification, we check that the language of traces of an implementation all belong to the language of a specification. We consider the refinement verification problem for asynchronous programs against specifications given by a Dyck language. We show that this problem is EXPSPACE-complete - the same complexity as that of language emptiness and for refinement verification against a regular specification. Our algorithm uses several technical ingredients. First, we show that checking if the coverability language of a succinctly described vector addition system with states (VASS) is contained in a Dyck language is EXPSPACE-complete. Second, in the more technical part of the proof, we define an ordering on words and show a downward closure construction that allows replacing the (context-free) language of each task in an asynchronous program by a regular language. Unlike downward closure operations usually considered in infinite-state verification, our ordering is not a well-quasi-ordering, and we have to construct the regular language ab initio. Once the tasks can be replaced, we show a reduction to an appropriate VASS and use our first ingredient. In addition to the inherent theoretical interest, refinement verification with Dyck specifications captures common practical resource usage patterns based on reference counting, for which few algorithmic techniques were known.
Cite as

Pascal Baumann, Moses Ganardi, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. Checking Refinement of Asynchronous Programs Against Context-Free Specifications. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 110:1-110:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{baumann_et_al:LIPIcs.ICALP.2023.110,
  author =	{Baumann, Pascal and Ganardi, Moses and Majumdar, Rupak and Thinniyam, Ramanathan S. and Zetzsche, Georg},
  title =	{{Checking Refinement of Asynchronous Programs Against Context-Free Specifications}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{110:1--110:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.110},
  URN =		{urn:nbn:de:0030-drops-181622},
  doi =		{10.4230/LIPIcs.ICALP.2023.110},
  annote =	{Keywords: Asynchronous programs, VASS, Dyck languages, Language inclusion, Refinement verification}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CONCUR.2022.4
Sequential Decision Making With Information Asymmetry (Invited Talk)

Authors: Jiarui Gan, Rupak Majumdar, Goran Radanovic, and Adish Singla

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
We survey some recent results in sequential decision making under uncertainty, where there is an information asymmetry among the decision-makers. We consider two versions of the problem: persuasion and mechanism design. In persuasion, a more-informed principal influences the actions of a less-informed agent by signaling information. In mechanism design, a less-informed principal incentivizes a more-informed agent to reveal information by committing to a mechanism, so that the principal can make more informed decisions. We define Markov persuasion processes and Markov mechanism processes that model persuasion and mechanism design into dynamic models. Then we survey results on optimal persuasion and optimal mechanism design on myopic and far-sighted agents. These problems are solvable in polynomial time for myopic agents but hard for far-sighted agents.
Cite as

Jiarui Gan, Rupak Majumdar, Goran Radanovic, and Adish Singla. Sequential Decision Making With Information Asymmetry (Invited Talk). In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{gan_et_al:LIPIcs.CONCUR.2022.4,
  author =	{Gan, Jiarui and Majumdar, Rupak and Radanovic, Goran and Singla, Adish},
  title =	{{Sequential Decision Making With Information Asymmetry}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{4:1--4:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.4},
  URN =		{urn:nbn:de:0030-drops-170673},
  doi =		{10.4230/LIPIcs.CONCUR.2022.4},
  annote =	{Keywords: Bayesian persuasion, Automated mechanism design, Markov persuasion processes, Markov mechanism processes, Myopic agents}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.40
The Pseudo-Reachability Problem for Diagonalisable Linear Dynamical Systems

Authors: Julian D'Costa, Toghrul Karimov, Rupak Majumdar, Joël Ouaknine, Mahmoud Salamati, and James Worrell

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
We study fundamental reachability problems on pseudo-orbits of linear dynamical systems. Pseudo-orbits can be viewed as a model of computation with limited precision and pseudo-reachability can be thought of as a robust version of classical reachability. Using an approach based on o-minimality of ℝ_exp we prove decidability of the discrete-time pseudo-reachability problem with arbitrary semialgebraic targets for diagonalisable linear dynamical systems. We also show that our method can be used to reduce the continuous-time pseudo-reachability problem to the (classical) time-bounded reachability problem, which is known to be conditionally decidable.
Cite as

Julian D'Costa, Toghrul Karimov, Rupak Majumdar, Joël Ouaknine, Mahmoud Salamati, and James Worrell. The Pseudo-Reachability Problem for Diagonalisable Linear Dynamical Systems. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 40:1-40:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{dcosta_et_al:LIPIcs.MFCS.2022.40,
  author =	{D'Costa, Julian and Karimov, Toghrul and Majumdar, Rupak and Ouaknine, Jo\"{e}l and Salamati, Mahmoud and Worrell, James},
  title =	{{The Pseudo-Reachability Problem for Diagonalisable Linear Dynamical Systems}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{40:1--40:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.40},
  URN =		{urn:nbn:de:0030-drops-168380},
  doi =		{10.4230/LIPIcs.MFCS.2022.40},
  annote =	{Keywords: pseudo-orbits, Orbit problem, Skolem problem, linear dynamical systems, reachability}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2022.124
Reachability in Bidirected Pushdown VASS

Authors: Moses Ganardi, Rupak Majumdar, Andreas Pavlogiannis, Lia Schütze, and Georg Zetzsche

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
A pushdown vector addition system with states (PVASS) extends the model of vector addition systems with a pushdown store. A PVASS is said to be bidirected if every transition (pushing/popping a symbol or modifying a counter) has an accompanying opposite transition that reverses the effect. Bidirectedness arises naturally in many models; it can also be seen as a overapproximation of reachability. We show that the reachability problem for bidirected PVASS is decidable in Ackermann time and primitive recursive for any fixed dimension. For the special case of one-dimensional bidirected PVASS, we show reachability is in PSPACE, and in fact in polynomial time if the stack is polynomially bounded. Our results are in contrast to the directed setting, where decidability of reachability is a long-standing open problem already for one dimensional PVASS, and there is a PSPACE-lower bound already for one-dimensional PVASS with bounded stack. The reachability relation in the bidirected (stateless) case is a congruence over ℕ^d. Our upper bounds exploit saturation techniques over congruences. In particular, we show novel elementary-time constructions of semilinear representations of congruences generated by finitely many vector pairs. In the case of one-dimensional PVASS, we employ a saturation procedure over bounded-size counters. We complement our upper bound with a TOWER-hardness result for arbitrary dimension and k-EXPSPACE hardness in dimension 2k+6 using a technique by Lazić and Totzke to implement iterative exponentiations.
Cite as

Moses Ganardi, Rupak Majumdar, Andreas Pavlogiannis, Lia Schütze, and Georg Zetzsche. Reachability in Bidirected Pushdown VASS. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 124:1-124:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{ganardi_et_al:LIPIcs.ICALP.2022.124,
  author =	{Ganardi, Moses and Majumdar, Rupak and Pavlogiannis, Andreas and Sch\"{u}tze, Lia and Zetzsche, Georg},
  title =	{{Reachability in Bidirected Pushdown VASS}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{124:1--124:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.124},
  URN =		{urn:nbn:de:0030-drops-164651},
  doi =		{10.4230/LIPIcs.ICALP.2022.124},
  annote =	{Keywords: Vector addition systems, Pushdown, Reachability, Decidability, Complexity}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.34
The Pseudo-Skolem Problem is Decidable

Authors: Julian D'Costa, Toghrul Karimov, Rupak Majumdar, Joël Ouaknine, Mahmoud Salamati, Sadegh Soudjani, and James Worrell

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
We study fundamental decision problems on linear dynamical systems in discrete time. We focus on pseudo-orbits, the collection of trajectories of the dynamical system for which there is an arbitrarily small perturbation at each step. Pseudo-orbits are generalizations of orbits in the topological theory of dynamical systems. We study the pseudo-orbit problem, whether a state belongs to the pseudo-orbit of another state, and the pseudo-Skolem problem, whether a hyperplane is reachable by an ε-pseudo-orbit for every ε. These problems are analogous to the well-studied orbit problem and Skolem problem on unperturbed dynamical systems. Our main results show that the pseudo-orbit problem is decidable in polynomial time and the Skolem problem on pseudo-orbits is decidable. The former extends the seminal result of Kannan and Lipton from orbits to pseudo-orbits. The latter is in contrast to the Skolem problem for linear dynamical systems, which remains open for proper orbits.
Cite as

Julian D'Costa, Toghrul Karimov, Rupak Majumdar, Joël Ouaknine, Mahmoud Salamati, Sadegh Soudjani, and James Worrell. The Pseudo-Skolem Problem is Decidable. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 34:1-34:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{dcosta_et_al:LIPIcs.MFCS.2021.34,
  author =	{D'Costa, Julian and Karimov, Toghrul and Majumdar, Rupak and Ouaknine, Jo\"{e}l and Salamati, Mahmoud and Soudjani, Sadegh and Worrell, James},
  title =	{{The Pseudo-Skolem Problem is Decidable}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{34:1--34:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.34},
  URN =		{urn:nbn:de:0030-drops-144742},
  doi =		{10.4230/LIPIcs.MFCS.2021.34},
  annote =	{Keywords: Pseudo-orbits, Orbit problem, Skolem problem, linear dynamical systems}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.35
Generalising Projection in Asynchronous Multiparty Session Types

Authors: Rupak Majumdar, Madhavan Mukund, Felix Stutz, and Damien Zufferey

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
Multiparty session types (MSTs) provide an efficient methodology for specifying and verifying message passing software systems. In the theory of MSTs, a global type specifies the interaction among the roles at the global level. A local specification for each role is generated by projecting from the global type on to the message exchanges it participates in. Whenever a global type can be projected on to each role, the composition of the projections is deadlock free and has exactly the behaviours specified by the global type. The key to the usability of MSTs is the projection operation: a more expressive projection allows more systems to be type-checked but requires a more difficult soundness argument. In this paper, we generalise the standard projection operation in MSTs. This allows us to model and type-check many design patterns in distributed systems, such as load balancing, that are rejected by the standard projection. The key to the new projection is an analysis that tracks causality between messages. Our soundness proof uses novel graph-theoretic techniques from the theory of message-sequence charts. We demonstrate the efficacy of the new projection operation by showing many global types for common patterns that can be projected under our projection but not under the standard projection operation.
Cite as

Rupak Majumdar, Madhavan Mukund, Felix Stutz, and Damien Zufferey. Generalising Projection in Asynchronous Multiparty Session Types. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 35:1-35:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{majumdar_et_al:LIPIcs.CONCUR.2021.35,
  author =	{Majumdar, Rupak and Mukund, Madhavan and Stutz, Felix and Zufferey, Damien},
  title =	{{Generalising Projection in Asynchronous Multiparty Session Types}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{35:1--35:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.35},
  URN =		{urn:nbn:de:0030-drops-144125},
  doi =		{10.4230/LIPIcs.CONCUR.2021.35},
  annote =	{Keywords: Multiparty session types, Verification, Communicating state machines}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ICALP.2021.1
From Verification to Causality-Based Explications (Invited Talk)

Authors: Christel Baier, Clemens Dubslaff, Florian Funke, Simon Jantsch, Rupak Majumdar, Jakob Piribauer, and Robin Ziemek

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
In view of the growing complexity of modern software architectures, formal models are increasingly used to understand why a system works the way it does, opposed to simply verifying that it behaves as intended. This paper surveys approaches to formally explicate the observable behavior of reactive systems. We describe how Halpern and Pearl’s notion of actual causation inspired verification-oriented studies of cause-effect relationships in the evolution of a system. A second focus lies on applications of the Shapley value to responsibility ascriptions, aimed to measure the influence of an event on an observable effect. Finally, formal approaches to probabilistic causation are collected and connected, and their relevance to the understanding of probabilistic systems is discussed.
Cite as

Christel Baier, Clemens Dubslaff, Florian Funke, Simon Jantsch, Rupak Majumdar, Jakob Piribauer, and Robin Ziemek. From Verification to Causality-Based Explications (Invited Talk). In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 1:1-1:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{baier_et_al:LIPIcs.ICALP.2021.1,
  author =	{Baier, Christel and Dubslaff, Clemens and Funke, Florian and Jantsch, Simon and Majumdar, Rupak and Piribauer, Jakob and Ziemek, Robin},
  title =	{{From Verification to Causality-Based Explications}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{1:1--1:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.1},
  URN =		{urn:nbn:de:0030-drops-140709},
  doi =		{10.4230/LIPIcs.ICALP.2021.1},
  annote =	{Keywords: Model Checking, Causality, Responsibility, Counterfactuals, Shapley value}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.32
Algebraic Invariants for Linear Hybrid Automata

Authors: Rupak Majumdar, Joël Ouaknine, Amaury Pouly, and James Worrell

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
We exhibit an algorithm to compute the strongest algebraic (or polynomial) invariants that hold at each location of a given guard-free linear hybrid automaton (i.e., a hybrid automaton having only unguarded transitions, all of whose assignments are given by affine expressions, and all of whose continuous dynamics are given by linear differential equations). Our main tool is a control-theoretic result of independent interest: given such a linear hybrid automaton, we show how to discretise the continuous dynamics in such a way that the resulting automaton has precisely the same algebraic invariants.
Cite as

Rupak Majumdar, Joël Ouaknine, Amaury Pouly, and James Worrell. Algebraic Invariants for Linear Hybrid Automata. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 32:1-32:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{majumdar_et_al:LIPIcs.CONCUR.2020.32,
  author =	{Majumdar, Rupak and Ouaknine, Jo\"{e}l and Pouly, Amaury and Worrell, James},
  title =	{{Algebraic Invariants for Linear Hybrid Automata}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{32:1--32:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.32},
  URN =		{urn:nbn:de:0030-drops-128443},
  doi =		{10.4230/LIPIcs.CONCUR.2020.32},
  annote =	{Keywords: Hybrid automata, algebraic invariants}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.111
The Complexity of Bounded Context Switching with Dynamic Thread Creation

Authors: Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Abstract
Dynamic networks of concurrent pushdown systems (DCPS) are a theoretical model for multi-threaded recursive programs with shared global state and dynamical creation of threads. The (global) state reachability problem for DCPS is undecidable in general, but Atig et al. (2009) showed that it becomes decidable, and is in 2EXPSPACE, when each thread is restricted to a fixed number of context switches. The best known lower bound for the problem is EXPSPACE-hard and this lower bound follows already when each thread is a finite-state machine and runs atomically to completion (i.e., does not switch contexts). In this paper, we close the gap by showing that state reachability is 2EXPSPACE-hard already with only one context switch. Interestingly, state reachability analysis is in EXPSPACE both for pushdown threads without context switches as well as for finite-state threads with arbitrary context switches. Thus, recursive threads together with a single context switch provide an exponential advantage. Our proof techniques are of independent interest for 2EXPSPACE-hardness results. We introduce transducer-defined Petri nets, a succinct representation for Petri nets, and show coverability is 2EXPSPACE-hard for this model. To show 2EXPSPACE-hardness, we present a modified version of Lipton’s simulation of counter machines by Petri nets, where the net programs can make explicit recursive procedure calls up to a bounded depth.
Cite as

Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. The Complexity of Bounded Context Switching with Dynamic Thread Creation. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 111:1-111:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{baumann_et_al:LIPIcs.ICALP.2020.111,
  author =	{Baumann, Pascal and Majumdar, Rupak and Thinniyam, Ramanathan S. and Zetzsche, Georg},
  title =	{{The Complexity of Bounded Context Switching with Dynamic Thread Creation}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{111:1--111:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.111},
  URN =		{urn:nbn:de:0030-drops-125187},
  doi =		{10.4230/LIPIcs.ICALP.2020.111},
  annote =	{Keywords: Dynamic thread creation, Bounded context switching, Asynchronous Programs, Safety verification, State reachability, Petri nets, Complexity, Succinctness, Counter Programs}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.133
On Decidability of Time-Bounded Reachability in CTMDPs

Authors: Rupak Majumdar, Mahmoud Salamati, and Sadegh Soudjani

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Abstract
We consider the time-bounded reachability problem for continuous-time Markov decision processes. We show that the problem is decidable subject to Schanuel’s conjecture. Our decision procedure relies on the structure of optimal policies and the conditional decidability (under Schanuel’s conjecture) of the theory of reals extended with exponential and trigonometric functions over bounded domains. We further show that any unconditional decidability result would imply unconditional decidability of the bounded continuous Skolem problem, or equivalently, the problem of checking if an exponential polynomial has a non-tangential zero in a bounded interval. We note that the latter problems are also decidable subject to Schanuel’s conjecture but finding unconditional decision procedures remain longstanding open problems.
Cite as

Rupak Majumdar, Mahmoud Salamati, and Sadegh Soudjani. On Decidability of Time-Bounded Reachability in CTMDPs. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 133:1-133:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{majumdar_et_al:LIPIcs.ICALP.2020.133,
  author =	{Majumdar, Rupak and Salamati, Mahmoud and Soudjani, Sadegh},
  title =	{{On Decidability of Time-Bounded Reachability in CTMDPs}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{133:1--133:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.133},
  URN =		{urn:nbn:de:0030-drops-125408},
  doi =		{10.4230/LIPIcs.ICALP.2020.133},
  annote =	{Keywords: CTMDP, Time bounded reachability, Continuous Skolem Problem, Schanuel’s Conjecture}
}
Document
Brave New Idea Paper
DOI: 10.4230/LIPIcs.ECOOP.2019.28
Motion Session Types for Robotic Interactions (Brave New Idea Paper)

Authors: Rupak Majumdar, Marcus Pirron, Nobuko Yoshida, and Damien Zufferey

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Abstract
Robotics applications involve programming concurrent components synchronising through messages while simultaneously executing motion primitives that control the state of the physical world. Today, these applications are typically programmed in low-level imperative programming languages which provide little support for abstraction or reasoning. We present a unifying programming model for concurrent message-passing systems that additionally control the evolution of physical state variables, together with a compositional reasoning framework based on multiparty session types. Our programming model combines message-passing concurrent processes with motion primitives. Processes represent autonomous components in a robotic assembly, such as a cart or a robotic arm, and they synchronise via discrete messages as well as via motion primitives. Continuous evolution of trajectories under the action of controllers is also modelled by motion primitives, which operate in global, physical time. We use multiparty session types as specifications to orchestrate discrete message-passing concurrency and continuous flow of trajectories. A global session type specifies the communication protocol among the components with joint motion primitives. A projection from a global type ensures that jointly executed actions at end-points are communication safe and deadlock-free, i.e., session-typed components do not get stuck. Together, these checks provide a compositional verification methodology for assemblies of robotic components with respect to concurrency invariants such as a progress property of communications as well as dynamic invariants such as absence of collision. We have implemented our core language and, through initial experiments, have shown how multiparty session types can be used to specify and compositionally verify robotic systems implemented on top of off-the-shelf and custom hardware using standard robotics application libraries.
Cite as

Rupak Majumdar, Marcus Pirron, Nobuko Yoshida, and Damien Zufferey. Motion Session Types for Robotic Interactions (Brave New Idea Paper). In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 28:1-28:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{majumdar_et_al:LIPIcs.ECOOP.2019.28,
  author =	{Majumdar, Rupak and Pirron, Marcus and Yoshida, Nobuko and Zufferey, Damien},
  title =	{{Motion Session Types for Robotic Interactions}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{28:1--28:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.28},
  URN =		{urn:nbn:de:0030-drops-108205},
  doi =		{10.4230/LIPIcs.ECOOP.2019.28},
  annote =	{Keywords: Session Types, Robotics, Concurrent Programming, Motions, Communications, Multiparty Session Types, Deadlock Freedom}
}
Document
DOI: 10.4230/LIPIcs.ECRTS.2019.9
From Iteration to System Failure: Characterizing the FITness of Periodic Weakly-Hard Systems

Authors: Arpan Gujarati, Mitra Nasri, Rupak Majumdar, and Björn B. Brandenburg

Published in: LIPIcs, Volume 133, 31st Euromicro Conference on Real-Time Systems (ECRTS 2019)

Abstract
Estimating metrics such as the Mean Time To Failure (MTTF) or its inverse, the Failures-In-Time (FIT), is a central problem in reliability estimation of safety-critical systems. To this end, prior work in the real-time and embedded systems community has focused on bounding the probability of failures in a single iteration of the control loop, resulting in, for example, the worst-case probability of a message transmission error due to electromagnetic interference, or an upper bound on the probability of a skipped or an incorrect actuation. However, periodic systems, which can be found at the core of most safety-critical real-time systems, are routinely designed to be robust to a single fault or to occasional failures (case in point, control applications are usually robust to a few skipped or misbehaving control loop iterations). Thus, obtaining long-run reliability metrics like MTTF and FIT from single iteration estimates by calculating the time to first fault can be quite pessimistic. Instead, overall system failures for such systems are better characterized using multi-state models such as weakly-hard constraints. In this paper, we describe and empirically evaluate three orthogonal approaches, PMC, Mart, and SAp, for the sound estimation of system’s MTTF, starting from a periodic stochastic model characterizing the failure in a single iteration of a periodic system, and using weakly-hard constraints as a measure of system robustness. PMC and Mart are exact analyses based on Markov chain analysis and martingale theory, respectively, whereas SAp is a sound approximation based on numerical analysis. We evaluate these techniques empirically in terms of their accuracy and numerical precision, their expressiveness for different definitions of weakly-hard constraints, and their space and time complexities, which affect their scalability and applicability in different regions of the space of weakly-hard constraints.
Cite as

Arpan Gujarati, Mitra Nasri, Rupak Majumdar, and Björn B. Brandenburg. From Iteration to System Failure: Characterizing the FITness of Periodic Weakly-Hard Systems. In 31st Euromicro Conference on Real-Time Systems (ECRTS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 133, pp. 9:1-9:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{gujarati_et_al:LIPIcs.ECRTS.2019.9,
  author =	{Gujarati, Arpan and Nasri, Mitra and Majumdar, Rupak and Brandenburg, Bj\"{o}rn B.},
  title =	{{From Iteration to System Failure: Characterizing the FITness of Periodic Weakly-Hard Systems}},
  booktitle =	{31st Euromicro Conference on Real-Time Systems (ECRTS 2019)},
  pages =	{9:1--9:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-110-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{133},
  editor =	{Quinton, Sophie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2019.9},
  URN =		{urn:nbn:de:0030-drops-107468},
  doi =		{10.4230/LIPIcs.ECRTS.2019.9},
  annote =	{Keywords: reliability analysis, MTTF/FIT analysis, weakly-hard constraints}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.FSTTCS.2018.1
Random Testing for Distributed Systems with Theoretical Guarantees (Invited Paper)

Authors: Rupak Majumdar

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

Abstract
Random testing has proven to be an effective way to catch bugs in concurrent and distributed systems. This is surprising, as the space of executions is enormous and conventional formal methods intuition would suggest that bad behaviors would only be found by extremely unlikely coincidences. Empirically, many bugs in distributed systems can be explained by interactions among only a small number of features. Thus, one can attempt to explain the effectiveness of random testing under various "small depth" hypotheses. In particular, it may be possible to test all interactions of k features for a small constant k by executing a family of tests that is exponentially or even doubly-exponentially smaller than the family of all tests. Moreover, under certain conditions, a randomly chosen small set of tests is sufficient to cover all k-wise interactions with high probability. I will describe two concrete scenarios. First, I will describe bugs in distributed systems caused by network partition faults. In many practical instances, these bugs occur due to two or three key nodes, such as leaders or replicas, not being able to communicate, or because the leading node finds itself in a block of the partition without quorum. In this case, I will show using the probabilistic method that a small set of randomly chosen tests will cover all "small partition" scenarios with high probability. Second, I will consider bugs that arise due to unexpected schedules (interleavings) of concurrent events. Again, many bugs depend only on the relative ordering of a small number of events (the "bug depth" of the bug). In this case, I will show a testing algorithm that prioritizes low depth interleavings and a randomized testing algorithm that bounds the probability of sampling any behavior of bug depth k for a fixed k. The testing algorithm is based on combinatorial insights from the theory of partial orders, such as the notion of dimension and its generalization to d-hitting families as well as results on online chain partitioning. Beyond the potential for designing or explaining random testing procedures, the technical arguments show the potential of combining "Theory A" and "Theory B" results to the important domain of software testing. This is joint work primarily with Filip Niksic [Filip Niksic, 2018], and with Dmitry Chistikov, Simin Oraee, Burcu Kulahcioglu Özkan, Mitra Tabaei Befrouei, and Georg Weissenbacher. This work was partially funded by an ERC Synergy Award (ImPACT).
Cite as

Rupak Majumdar. Random Testing for Distributed Systems with Theoretical Guarantees (Invited Paper). In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{majumdar:LIPIcs.FSTTCS.2018.1,
  author =	{Majumdar, Rupak},
  title =	{{Random Testing for Distributed Systems with Theoretical Guarantees}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.1},
  URN =		{urn:nbn:de:0030-drops-99000},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.1},
  annote =	{Keywords: Random testing, Hitting families}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.31
Verification of Immediate Observation Population Protocols

Authors: Javier Esparza, Pierre Ganty, Rupak Majumdar, and Chana Weil-Kennedy

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

Abstract
Population protocols (Angluin et al., PODC, 2004) are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their states. Computations are infinite sequences of interactions satisfying a strong fairness constraint. A population protocol is well-specified if for every initial configuration C of devices, and every computation starting at C, all devices eventually agree on a consensus value depending only on C. If a protocol is well-specified, then it is said to compute the predicate that assigns to each initial configuration its consensus value. In a previous paper we have shown that the problem whether a given protocol is well-specified and the problem whether it computes a given predicate are decidable. However, in the same paper we prove that both problems are at least as hard as the reachability problem for Petri nets. Since all known algorithms for Petri net reachability have non-primitive recursive complexity, in this paper we restrict attention to immediate observation (IO) population protocols, a class introduced and studied in (Angluin et al., PODC, 2006). We show that both problems are solvable in exponential space for IO protocols. This is the first syntactically defined, interesting class of protocols for which an algorithm not requiring Petri net reachability is found.
Cite as

Javier Esparza, Pierre Ganty, Rupak Majumdar, and Chana Weil-Kennedy. Verification of Immediate Observation Population Protocols. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.CONCUR.2018.31,
  author =	{Esparza, Javier and Ganty, Pierre and Majumdar, Rupak and Weil-Kennedy, Chana},
  title =	{{Verification of Immediate Observation Population Protocols}},
  booktitle =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  pages =	{31:1--31:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.31},
  URN =		{urn:nbn:de:0030-drops-95695},
  doi =		{10.4230/LIPIcs.CONCUR.2018.31},
  annote =	{Keywords: Population protocols, Immediate Observation, Parametrized verification}
}
Document
DOI: 10.4230/DagRep.7.5.84
Formal Synthesis of Cyber-Physical Systems (Dagstuhl Seminar 17201)

Authors: Calin A. Belta, Rupak Majumdar, Maijid Zamani, and Matthias Rungger

Published in: Dagstuhl Reports, Volume 7, Issue 5 (2018)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 17201 "Formal Synthesis of Cyber-Physical Systems." Formal synthesis is the application of algorithmic techniques based on automata and logic to the design of controllers for hybrid systems in which continuous components interact with discrete ones. The Dagstuhl seminar brought together researchers from control theory and from computer science to discuss the state-of-the-art and current challenges in the field.
Cite as

Calin A. Belta, Rupak Majumdar, Maijid Zamani, and Matthias Rungger. Formal Synthesis of Cyber-Physical Systems (Dagstuhl Seminar 17201). In Dagstuhl Reports, Volume 7, Issue 5, pp. 84-96, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{belta_et_al:DagRep.7.5.84,
  author =	{Belta, Calin A. and Majumdar, Rupak and Zamani, Maijid and Rungger, Matthias},
  title =	{{Formal Synthesis of Cyber-Physical Systems (Dagstuhl Seminar 17201)}},
  pages =	{84--96},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2017},
  volume =	{7},
  number =	{5},
  editor =	{Belta, Calin A. and Majumdar, Rupak and Zamani, Maijid and Rungger, Matthias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.7.5.84},
  URN =		{urn:nbn:de:0030-drops-82813},
  doi =		{10.4230/DagRep.7.5.84},
  annote =	{Keywords: Cyber-physical systems, formal synthesis, reactive synthesis, discrete event systems, dynamical systems and control}
}
Document
DOI: 10.4230/DagRep.7.3.27
Game Theory in AI, Logic, and Algorithms (Dagstuhl Seminar 17111)

Authors: Swarat Chaudhuri, Sampath Kannan, Rupak Majumdar, and Michael J. Wooldridge

Published in: Dagstuhl Reports, Volume 7, Issue 3 (2017)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 17111 "Game Theory in AI, Logic, and Algorithms".
Cite as

Swarat Chaudhuri, Sampath Kannan, Rupak Majumdar, and Michael J. Wooldridge. Game Theory in AI, Logic, and Algorithms (Dagstuhl Seminar 17111). In Dagstuhl Reports, Volume 7, Issue 3, pp. 27-32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{chaudhuri_et_al:DagRep.7.3.27,
  author =	{Chaudhuri, Swarat and Kannan, Sampath and Majumdar, Rupak and Wooldridge, Michael J.},
  title =	{{Game Theory in AI, Logic, and Algorithms (Dagstuhl Seminar 17111)}},
  pages =	{27--32},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2017},
  volume =	{7},
  number =	{3},
  editor =	{Chaudhuri, Swarat and Kannan, Sampath and Majumdar, Rupak and Wooldridge, Michael J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.7.3.27},
  URN =		{urn:nbn:de:0030-drops-79609},
  doi =		{10.4230/DagRep.7.3.27},
  annote =	{Keywords: game theory, formal methods, logic, algorithms, equilibria, multiagent systems}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.13
The Robot Routing Problem for Collecting Aggregate Stochastic Rewards

Authors: Rayna Dimitrova, Ivan Gavran, Rupak Majumdar, Vinayak S. Prabhu, and Sadegh Esmaeil Zadeh Soudjani

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
We propose a new model for formalizing reward collection problems on graphs with dynamically generated rewards which may appear and disappear based on a stochastic model. The robot routing problem is modeled as a graph whose nodes are stochastic processes generating potential rewards over discrete time. The rewards are generated according to the stochastic process, but at each step, an existing reward disappears with a given probability. The edges in the graph encode the (unit-distance) paths between the rewards' locations. On visiting a node, the robot collects the accumulated reward at the node at that time, but traveling between the nodes takes time. The optimization question asks to compute an optimal (or epsilon-optimal) path that maximizes the expected collected rewards. We consider the finite and infinite-horizon robot routing problems. For finite-horizon, the goal is to maximize the total expected reward, while for infinite horizon we consider limit-average objectives. We study the computational and strategy complexity of these problems, establish NP-lower bounds and show that optimal strategies require memory in general. We also provide an algorithm for computing epsilon-optimal infinite paths for arbitrary epsilon > 0.
Cite as

Rayna Dimitrova, Ivan Gavran, Rupak Majumdar, Vinayak S. Prabhu, and Sadegh Esmaeil Zadeh Soudjani. The Robot Routing Problem for Collecting Aggregate Stochastic Rewards. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{dimitrova_et_al:LIPIcs.CONCUR.2017.13,
  author =	{Dimitrova, Rayna and Gavran, Ivan and Majumdar, Rupak and Prabhu, Vinayak S. and Soudjani, Sadegh Esmaeil Zadeh},
  title =	{{The Robot Routing Problem for Collecting Aggregate Stochastic Rewards}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{13:1--13:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.13},
  URN =		{urn:nbn:de:0030-drops-77920},
  doi =		{10.4230/LIPIcs.CONCUR.2017.13},
  annote =	{Keywords: Path Planning, Graph Games, Quantitative Objectives, Discounting}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2016.27
Model Checking Population Protocols

Authors: Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

Abstract
Population protocols are a model for parameterized systems in which a set of identical, anonymous, finite-state processes interact pairwise through rendezvous synchronization. In each step, the pair of interacting processes is chosen by a random scheduler. Angluin et al. (PODC 2004) studied population protocols as a distributed computation model. They characterized the computational power in the limit (semi-linear predicates) of a subclass of protocols (the well-specified ones). However, the modeling power of protocols go beyond computation of semi-linear predicates and they can be used to study a wide range of distributed protocols, such as asynchronous leader election or consensus, stochastic evolutionary processes, or chemical reaction networks. Correspondingly, one is interested in checking specifications on these protocols that go beyond the well-specified computation of predicates. In this paper, we characterize the decidability frontier for the model checking problem for population protocols against probabilistic linear-time specifications. We show that the model checking problem is decidable for qualitative objectives, but as hard as the reachability problem for Petri nets - a well-known hard problem without known elementary algorithms. On the other hand, model checking is undecidable for quantitative properties.
Cite as

Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Model Checking Population Protocols. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 27:1-27:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.FSTTCS.2016.27,
  author =	{Esparza, Javier and Ganty, Pierre and Leroux, J\'{e}r\^{o}me and Majumdar, Rupak},
  title =	{{Model Checking Population Protocols}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{27:1--27:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.27},
  URN =		{urn:nbn:de:0030-drops-68628},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.27},
  annote =	{Keywords: parameterized systems, population protocols, probabilistic model checking, probabilistic linear-time specifications, decidability}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.169
Dynamic Bayesian Networks as Formal Abstractions of Structured Stochastic Processes

Authors: Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate, and Rupak Majumdar

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
We study the problem of finite-horizon probabilistic invariance for discrete-time Markov processes over general (uncountable) state spaces. We compute discrete-time, finite-state Markov chains as formal abstractions of general Markov processes. Our abstraction differs from existing approaches in two ways. First, we exploit the structure of the underlying Markov process to compute the abstraction separately for each dimension. Second, we employ dynamic Bayesian networks (DBN) as compact representations of the abstraction. In contrast, existing approaches represent and store the (exponentially large) Markov chain explicitly, which leads to heavy memory requirements limiting the application to models of dimension less than half, according to our experiments. We show how to construct a DBN abstraction of a Markov process satisfying an independence assumption on the driving process noise. We compute a guaranteed bound on the error in the abstraction w.r.t. the probabilistic invariance property; the dimension-dependent abstraction makes the error bounds more precise than existing approaches. Additionally, we show how factor graphs and the sum-product algorithm for DBNs can be used to solve the finite-horizon probabilistic invariance problem. Together, DBN-based representations and algorithms can be significantly more efficient than explicit representations of Markov chains for abstracting and model checking structured Markov processes.
Cite as

Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate, and Rupak Majumdar. Dynamic Bayesian Networks as Formal Abstractions of Structured Stochastic Processes. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 169-183, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{esmaeilzadehsoudjani_et_al:LIPIcs.CONCUR.2015.169,
  author =	{Esmaeil Zadeh Soudjani, Sadegh and Abate, Alessandro and Majumdar, Rupak},
  title =	{{Dynamic Bayesian Networks as Formal Abstractions of Structured Stochastic Processes}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{169--183},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.169},
  URN =		{urn:nbn:de:0030-drops-53693},
  doi =		{10.4230/LIPIcs.CONCUR.2015.169},
  annote =	{Keywords: Structured stochastic systems, general space Markov processes, formal verification, dynamic Bayesian networks, Markov chain abstraction}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.470
Verification of Population Protocols

Authors: Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
Population protocols [Angluin et al., PODC, 2004] are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their states. Computations are infinite sequences of interactions satisfying a strong fairness constraint. A population protocol is well-specified if for every initial configuration C of devices, and every computation starting at C, all devices eventually agree on a consensus value depending only on C. If a protocol is well-specified, then it is said to compute the predicate that assigns to each initial configuration its consensus value. While the predicates computable by well-specified protocols have been extensively studied, the two basic verification problems remain open: is a given protocol well-specified? Does a protocol compute a given predicate? We prove that both problems are decidable. Our results also prove decidability of a natural question about home spaces of Petri nets.
Cite as

Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Verification of Population Protocols. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 470-482, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{esparza_et_al:LIPIcs.CONCUR.2015.470,
  author =	{Esparza, Javier and Ganty, Pierre and Leroux, J\'{e}r\^{o}me and Majumdar, Rupak},
  title =	{{Verification of Population Protocols}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{470--482},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.470},
  URN =		{urn:nbn:de:0030-drops-53770},
  doi =		{10.4230/LIPIcs.CONCUR.2015.470},
  annote =	{Keywords: Population protocols, Petri nets, parametrized verification}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.483
Rely/Guarantee Reasoning for Asynchronous Programs

Authors: Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, and Viktor Vafeiadis

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
Asynchronous programming has become ubiquitous in smartphone and web application development, as well as in the development of server-side and system applications. Many of the uses of asynchrony can be modeled by extending programming languages with asynchronous procedure calls - procedures not executed immediately, but stored and selected for execution at a later point by a non-deterministic scheduler. Asynchronous calls induce a flow of control that is difficult to reason about, which in turn makes formal verification of asynchronous programs challenging. In response, we take a rely/guarantee approach: Each asynchronous procedure is verified separately with respect to its rely and guarantee predicates; the correctness of the whole program then follows from the natural conditions the rely/guarantee predicates have to satisfy. In this way, the verification of asynchronous programs is modularly decomposed into the more usual verification of sequential programs with synchronous calls. For the sequential program verification we use Hoare-style deductive reasoning, which we demonstrate on several simplified examples. These examples were inspired from programs written in C using the popular Libevent library; they are manually annotated and verified within the state-of-the-art Frama-C platform.
Cite as

Ivan Gavran, Filip Niksic, Aditya Kanade, Rupak Majumdar, and Viktor Vafeiadis. Rely/Guarantee Reasoning for Asynchronous Programs. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 483-496, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{gavran_et_al:LIPIcs.CONCUR.2015.483,
  author =	{Gavran, Ivan and Niksic, Filip and Kanade, Aditya and Majumdar, Rupak and Vafeiadis, Viktor},
  title =	{{Rely/Guarantee Reasoning for Asynchronous Programs}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{483--496},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.483},
  URN =		{urn:nbn:de:0030-drops-53902},
  doi =		{10.4230/LIPIcs.CONCUR.2015.483},
  annote =	{Keywords: Asynchronous programs, rely/guarantee reasoning}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2015.396
Asynchronous Liquid Separation Types

Authors: Johannes Kloos, Rupak Majumdar, and Viktor Vafeiadis

Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)

Abstract
We present a refinement type system for reasoning about asynchronous programs manipulating shared mutable state. Our type system guarantees the absence of races and the preservation of user-specified invariants using a combination of two ideas: refinement types and concurrent separation logic. Our type system allows precise reasoning about programs using two ingredients. First, our types are indexed by sets of resource names and the type system tracks the effect of program execution on individual heap locations and task handles. In particular, it allows making strong updates to the types of heap locations. Second, our types track ownership of shared state across concurrently posted tasks and allow reasoning about ownership transfer between tasks using permissions. We demonstrate through several examples that these two ingredients, on top of the framework of liquid types, are powerful enough to reason about correct behavior of practical, complex, asynchronous systems manipulating shared heap resources. We have implemented type inference for our type system and have used it to prove complex invariants of asynchronous OCaml programs. We also show how the type system detects subtle concurrency bugs in a file system implementation.
Cite as

Johannes Kloos, Rupak Majumdar, and Viktor Vafeiadis. Asynchronous Liquid Separation Types. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 396-420, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{kloos_et_al:LIPIcs.ECOOP.2015.396,
  author =	{Kloos, Johannes and Majumdar, Rupak and Vafeiadis, Viktor},
  title =	{{Asynchronous Liquid Separation Types}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{396--420},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.396},
  URN =		{urn:nbn:de:0030-drops-52233},
  doi =		{10.4230/LIPIcs.ECOOP.2015.396},
  annote =	{Keywords: Liquid Types, Asynchronous Parallelism, Separation Logic, Type Systems}
}
Document
DOI: 10.4230/DagRep.4.3.85
Verification of Cyber-Physical Systems (Dagstuhl Seminar 14122)

Authors: Rupak Majumdar, Richard M. Murray, and Pavithra Prabhakar

Published in: Dagstuhl Reports, Volume 4, Issue 3 (2014)

Abstract
Cyber-physical systems refer to a new genre of engineered systems consisting of a tight coupling between computation, communication and physical entities. The main focus of the seminar was to discuss issues related to the reliable development of cyber-physical systems by using formal verification. This is a multi-disciplinary area requiring collaboration between areas focusing discrete systems analysis and continuous systems analysis. To this end, the seminar brought together researchers working in the fields of formal methods, control theory and hybrid systems to identify and discuss potential issues and research questions which require collaboration between the communities. This report documents the program and the outcomes of Dagstuhl Seminar 14122 "Verification of Cyber-Physical Systems".
Cite as

Rupak Majumdar, Richard M. Murray, and Pavithra Prabhakar. Verification of Cyber-Physical Systems (Dagstuhl Seminar 14122). In Dagstuhl Reports, Volume 4, Issue 3, pp. 85-102, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{majumdar_et_al:DagRep.4.3.85,
  author =	{Majumdar, Rupak and Murray, Richard M. and Prabhakar, Pavithra},
  title =	{{Verification of Cyber-Physical Systems (Dagstuhl Seminar 14122)}},
  pages =	{85--102},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{4},
  number =	{3},
  editor =	{Majumdar, Rupak and Murray, Richard M. and Prabhakar, Pavithra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.4.3.85},
  URN =		{urn:nbn:de:0030-drops-45937},
  doi =		{10.4230/DagRep.4.3.85},
  annote =	{Keywords: Formal Verification, Cyber-Physical Systems, Hybrid Systems}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2013.127
A Theory of Partitioned Global Address Spaces

Authors: Georgel Calin, Egor Derevenetc, Rupak Majumdar, and Roland Meyer

Published in: LIPIcs, Volume 24, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)

Abstract
Partitioned global address space (PGAS) is a parallel programming model for the development of high-performance applications on clusters. It provides a global address space partitioned among the cluster nodes, and is supported in programming languages like C, C++, and Fortran by means of APIs. Our first contribution is a formal model for the semantics of single program, multiple data programs that use PGAS APIs. Our model reflects the main features of popular real-world APIs such as SHMEM, ARMCI, GASNet, GPI, and GASPI. A key feature of PGAS is the support for one-sided communication: a node may directly read and write the memory located at a remote node, without explicit synchronization with the processes running on the remote side. One-sided communication increases performance by decoupling process synchronization from data transfer, but requires the programmer to reason about appropriate synchronizations between reads and writes. As a second contribution, we propose and investigate robustness, a criterion for correct synchronization of PGAS programs. Robustness corresponds to acyclicity of a suitable happens-before relation defined on PGAS computations. The requirement is finer than classical data race freedom and rules out most false error reports. Our main technical result is an algorithm for checking robustness of PGAS programs. The algorithm makes use of two insights. We first show that, if a PGAS program is not robust, then there are computations in a certain normal form that violate happens-before acyclicity. Intuitively, normal-form computations delay remote accesses in an ordered way. We then devise an algorithm that checks for cyclic normal-form computations. Essentially, the algorithm is an emptiness check for a novel automaton model that accepts normal-form computations in streaming fashion. Altogether, we prove that the robustness problem is PSPACE complete.
Cite as

Georgel Calin, Egor Derevenetc, Rupak Majumdar, and Roland Meyer. A Theory of Partitioned Global Address Spaces. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 127-139, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{calin_et_al:LIPIcs.FSTTCS.2013.127,
  author =	{Calin, Georgel and Derevenetc, Egor and Majumdar, Rupak and Meyer, Roland},
  title =	{{A Theory of Partitioned Global Address Spaces}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)},
  pages =	{127--139},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-64-4},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{24},
  editor =	{Seth, Anil and Vishnoi, Nisheeth K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2013.127},
  URN =		{urn:nbn:de:0030-drops-43665},
  doi =		{10.4230/LIPIcs.FSTTCS.2013.127},
  annote =	{Keywords: PGAS, SC preservation, Robustness, Semantics, Formal languages}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2008.1745
Algorithms for Game Metrics

Authors: Krishnendu Chatterjee, Luca de Alfaro, Rupak Majumdar, and Vishwanath Raman

Published in: LIPIcs, Volume 2, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2008)

Abstract
Simulation and bisimulation metrics for stochastic systems provide a quantitative generalization of the classical simulation and bisimulation relations. These metrics capture the similarity of states with respect to quantitative specifications written in the quantitative $\mu$-calculus and related probabilistic logics. We present algorithms for computing the metrics on Markov decision processes (MDPs), turn-based stochastic games, and concurrent games. For turn-based games and MDPs, we provide a polynomial-time algorithm based on linear programming for the computation of the one-step metric distance between states. The algorithm improves on the previously known exponential-time algorithm based on a reduction to the theory of reals. We then present PSPACE algorithms for both the decision problem and the problem of approximating the metric distance between two states, matching the best known bound for Markov chains. For the bisimulation kernel of the metric, which corresponds to probabilistic bisimulation, our algorithm works in time $\calo(n^4)$ for both turn-based games and MDPs; improving the previously best known $\calo(n^9\cdot\log(n))$ time algorithm for MDPs. For a concurrent game $G$, we show that computing the exact distance between states is at least as hard as computing the value of concurrent reachability games and the square-root-sum problem in computational geometry. We show that checking whether the metric distance is bounded by a rational $r$, can be accomplished via a reduction to the theory of real closed fields, involving a formula with three quantifier alternations, yielding $\calo(|G|^{\calo(|G|^5)})$ time complexity, improving the previously known reduction with $\calo(|G|^{\calo(|G|^7)})$ time complexity. These algorithms can be iterated to approximate the metrics using binary search.
Cite as

Krishnendu Chatterjee, Luca de Alfaro, Rupak Majumdar, and Vishwanath Raman. Algorithms for Game Metrics. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 2, pp. 107-118, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.FSTTCS.2008.1745,
  author =	{Chatterjee, Krishnendu and de Alfaro, Luca and Majumdar, Rupak and Raman, Vishwanath},
  title =	{{Algorithms for Game Metrics}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{107--118},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-08-8},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{2},
  editor =	{Hariharan, Ramesh and Mukund, Madhavan and Vinay, V},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2008.1745},
  URN =		{urn:nbn:de:0030-drops-17455},
  doi =		{10.4230/LIPIcs.FSTTCS.2008.1745},
  annote =	{Keywords: Algorithms, Metrics, Kernel, Simulation, Bisimulation, Linear Programming, Theory of Reals}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact